Termination proof of /tmp/tmpvhAxbp/A05.itrs

Termination of the given ITRSProblem could successfully be proven:

↳ ITRS

  ↳ ITRStoIDPProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

cond(TRUE, x, y) → +@z(1@z, minus(x, +@z(y, 1@z)))
min(u, v) → if(<@z(u, v), u, v)
if(FALSE, u, v) → v
if(TRUE, u, v) → u
minus(x, x) → 0@z
minus(x, y) → cond(=@z(min(x, y), y), x, y)

The set Q consists of the following terms:

cond(TRUE, x0, x1)
min(x0, x1)
if(FALSE, x0, x1)
if(TRUE, x0, x1)
minus(x0, x1)

Added dependency pairs

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

cond(TRUE, x, y) → +@z(1@z, minus(x, +@z(y, 1@z)))
min(u, v) → if(<@z(u, v), u, v)
if(FALSE, u, v) → v
if(TRUE, u, v) → u
minus(x, x) → 0@z
minus(x, y) → cond(=@z(min(x, y), y), x, y)

The integer pair graph contains the following rules and edges:

(0): MINUS(x[0], y[0]) → MIN(x[0], y[0])
(1): MINUS(x[1], y[1]) → COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1])
(2): MIN(u[2], v[2]) → IF(<@z(u[2], v[2]), u[2], v[2])
(3): COND(TRUE, x[3], y[3]) → MINUS(x[3], +@z(y[3], 1@z))

(0) -> (2), if ((y[0] →^* v[2])∧(x[0] →^* u[2]))

(1) -> (3), if ((x[1] →^* x[3])∧(y[1] →^* y[3])∧(=@z(min(x[1], y[1]), y[1]) →^* TRUE))

(3) -> (0), if ((+@z(y[3], 1@z) →^* y[0])∧(x[3] →^* x[0]))

(3) -> (1), if ((+@z(y[3], 1@z) →^* y[1])∧(x[3] →^* x[1]))

The set Q consists of the following terms:

cond(TRUE, x0, x1)
min(x0, x1)
if(FALSE, x0, x1)
if(TRUE, x0, x1)
minus(x0, x1)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

min(u, v) → if(<@z(u, v), u, v)
if(FALSE, u, v) → v
if(TRUE, u, v) → u

(0) -> (2), if ((y[0] →^* v[2])∧(x[0] →^* u[2]))

(1) -> (3), if ((x[1] →^* x[3])∧(y[1] →^* y[3])∧(=@z(min(x[1], y[1]), y[1]) →^* TRUE))

(3) -> (0), if ((+@z(y[3], 1@z) →^* y[0])∧(x[3] →^* x[0]))

(3) -> (1), if ((+@z(y[3], 1@z) →^* y[1])∧(x[3] →^* x[1]))

The set Q consists of the following terms:

cond(TRUE, x0, x1)
min(x0, x1)
if(FALSE, x0, x1)
if(TRUE, x0, x1)
minus(x0, x1)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPNonInfProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

min(u, v) → if(<@z(u, v), u, v)
if(FALSE, u, v) → v
if(TRUE, u, v) → u

The integer pair graph contains the following rules and edges:

(1): MINUS(x[1], y[1]) → COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1])
(3): COND(TRUE, x[3], y[3]) → MINUS(x[3], +@z(y[3], 1@z))

(1) -> (3), if ((x[1] →^* x[3])∧(y[1] →^* y[3])∧(=@z(min(x[1], y[1]), y[1]) →^* TRUE))

(3) -> (1), if ((+@z(y[3], 1@z) →^* y[1])∧(x[3] →^* x[1]))

The set Q consists of the following terms:

cond(TRUE, x0, x1)
min(x0, x1)
if(FALSE, x0, x1)
if(TRUE, x0, x1)
minus(x0, x1)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair MINUS(x[1], y[1]) → COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1]) the following chains were created:

We consider the chain MINUS(x[1], y[1]) → COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1]) which results in the following constraint:
(1)    (MINUS(x[1], y[1])≥NonInfC∧MINUS(x[1], y[1])≥COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1])∧(U^Increasing(COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1])), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1])), ≥)∧0 ≥ 0∧0 ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1])), ≥)∧0 ≥ 0∧0 ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1])), ≥)∧0 ≥ 0∧0 ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0)

For Pair COND(TRUE, x[3], y[3]) → MINUS(x[3], +@z(y[3], 1@z)) the following chains were created:

We consider the chain MINUS(x[1], y[1]) → COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1]), COND(TRUE, x[3], y[3]) → MINUS(x[3], +@z(y[3], 1@z)), MINUS(x[1], y[1]) → COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1]) which results in the following constraint:
(6)    (=@z(min(x[1], y[1]), y[1])=TRUE∧y[1]=y[3]∧+@z(y[3], 1@z)=y[1]1∧x[3]=x[1]1∧x[1]=x[3] ⇒ COND(TRUE, x[3], y[3])≥NonInfC∧COND(TRUE, x[3], y[3])≥MINUS(x[3], +@z(y[3], 1@z))∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥))

We simplified constraint (6) using rules (III), (IV), (VII), (IDP_BOOLEAN), (REWRITING) which results in the following new constraint:
(7)    (<@z(x[1], y[1])=x1∧if(x1, x[1], y[1])=x0 @ PF>=@z_2∧>=@z(x0, y[1])=TRUE∧<@z(x[1], y[1])=x3∧if(x3, x[1], y[1])=x2 @ PF<=@z_2∧<=@z(x2, y[1])=TRUE ⇒ COND(TRUE, x[1], y[1])≥NonInfC∧COND(TRUE, x[1], y[1])≥MINUS(x[1], +@z(y[1], 1@z))∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥))

We simplified constraint (7) using rule (V) (with possible (I) afterwards) using induction on if(x1, x[1], y[1])=x0 @ PF>=@z_2 which results in the following new constraints:
(8)    (x4=x0 @ PF>=@z_2∧<@z(x5, x4)=FALSE∧>=@z(x0, x4)=TRUE∧<@z(x5, x4)=x3∧if(x3, x5, x4)=x2 @ PF<=@z_2∧<=@z(x2, x4)=TRUE ⇒ COND(TRUE, x5, x4)≥NonInfC∧COND(TRUE, x5, x4)≥MINUS(x5, +@z(x4, 1@z))∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥))

(9)    (x7=x0 @ PF>=@z_2∧<@z(x7, x6)=TRUE∧>=@z(x0, x6)=TRUE∧<@z(x7, x6)=x3∧if(x3, x7, x6)=x2 @ PF<=@z_2∧<=@z(x2, x6)=TRUE ⇒ COND(TRUE, x7, x6)≥NonInfC∧COND(TRUE, x7, x6)≥MINUS(x7, +@z(x6, 1@z))∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥))

We simplified constraint (8) using rule (V) (with possible (I) afterwards) using induction on if(x3, x5, x4)=x2 @ PF<=@z_2 which results in the following new constraints:
(10)    (x8=x2 @ PF<=@z_2∧x8=x0 @ PF>=@z_2∧<@z(x9, x8)=FALSE∧>=@z(x0, x8)=TRUE∧<=@z(x2, x8)=TRUE ⇒ COND(TRUE, x9, x8)≥NonInfC∧COND(TRUE, x9, x8)≥MINUS(x9, +@z(x8, 1@z))∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥))

(11)    (x11=x2 @ PF<=@z_2∧x10=x0 @ PF>=@z_2∧<@z(x11, x10)=FALSE∧>=@z(x0, x10)=TRUE∧<@z(x11, x10)=TRUE∧<=@z(x2, x10)=TRUE ⇒ COND(TRUE, x11, x10)≥NonInfC∧COND(TRUE, x11, x10)≥MINUS(x11, +@z(x10, 1@z))∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥))

We simplified constraint (9) using rule (V) (with possible (I) afterwards) using induction on if(x3, x7, x6)=x2 @ PF<=@z_2 which results in the following new constraints:
(12)    (x12=x2 @ PF<=@z_2∧x13=x0 @ PF>=@z_2∧<@z(x13, x12)=TRUE∧>=@z(x0, x12)=TRUE∧<@z(x13, x12)=FALSE∧<=@z(x2, x12)=TRUE ⇒ COND(TRUE, x13, x12)≥NonInfC∧COND(TRUE, x13, x12)≥MINUS(x13, +@z(x12, 1@z))∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥))

(13)    (x15=x2 @ PF<=@z_2∧x15=x0 @ PF>=@z_2∧<@z(x15, x14)=TRUE∧>=@z(x0, x14)=TRUE∧<=@z(x2, x14)=TRUE ⇒ COND(TRUE, x15, x14)≥NonInfC∧COND(TRUE, x15, x14)≥MINUS(x15, +@z(x14, 1@z))∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥))

We simplified constraint (10) using rule (III) which results in the following new constraint:
(14)    (<@z(x9, x0)=FALSE∧>=@z(x0, x0)=TRUE∧<=@z(x0, x0)=TRUE ⇒ COND(TRUE, x9, x0)≥NonInfC∧COND(TRUE, x9, x0)≥MINUS(x9, +@z(x0, 1@z))∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥))

We simplified constraint (11) using rule (III) which results in the following new constraint:
(15)    (<@z(x2, x0)=FALSE∧>=@z(x0, x0)=TRUE∧<@z(x2, x0)=TRUE∧<=@z(x2, x0)=TRUE ⇒ COND(TRUE, x2, x0)≥NonInfC∧COND(TRUE, x2, x0)≥MINUS(x2, +@z(x0, 1@z))∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥))

We simplified constraint (12) using rule (III) which results in the following new constraint:
(16)    (<@z(x0, x2)=TRUE∧>=@z(x0, x2)=TRUE∧<@z(x0, x2)=FALSE∧<=@z(x2, x2)=TRUE ⇒ COND(TRUE, x0, x2)≥NonInfC∧COND(TRUE, x0, x2)≥MINUS(x0, +@z(x2, 1@z))∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥))

We simplified constraint (13) using rule (III) which results in the following new constraint:
(17)    (<@z(x0, x14)=TRUE∧>=@z(x0, x14)=TRUE∧<=@z(x0, x14)=TRUE ⇒ COND(TRUE, x0, x14)≥NonInfC∧COND(TRUE, x0, x14)≥MINUS(x0, +@z(x14, 1@z))∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥))

We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(18)    (x9 + (-1)x0 ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + (-1)x0 + x9 ≥ 0∧0 ≥ 0)

We simplified constraint (15) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(19)    (x2 + (-1)x0 ≥ 0∧0 ≥ 0∧-1 + x0 + (-1)x2 ≥ 0∧x0 + (-1)x2 ≥ 0 ⇒ (U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + (-1)x0 + x2 ≥ 0∧0 ≥ 0)

We simplified constraint (16) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(20)    (-1 + x2 + (-1)x0 ≥ 0∧x0 + (-1)x2 ≥ 0∧x0 + (-1)x2 ≥ 0∧0 ≥ 0 ⇒ (U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + (-1)x2 + x0 ≥ 0∧0 ≥ 0)

We simplified constraint (17) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(21)    (x14 + -1 + (-1)x0 ≥ 0∧x0 + (-1)x14 ≥ 0∧x14 + (-1)x0 ≥ 0 ⇒ (U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + (-1)x14 + x0 ≥ 0∧0 ≥ 0)

We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(22)    (x14 + -1 + (-1)x0 ≥ 0∧x0 + (-1)x14 ≥ 0∧x14 + (-1)x0 ≥ 0 ⇒ (U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + (-1)x14 + x0 ≥ 0∧0 ≥ 0)

We simplified constraint (18) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(23)    (x9 + (-1)x0 ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + (-1)x0 + x9 ≥ 0∧0 ≥ 0)

We simplified constraint (20) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(24)    (-1 + x2 + (-1)x0 ≥ 0∧x0 + (-1)x2 ≥ 0∧x0 + (-1)x2 ≥ 0∧0 ≥ 0 ⇒ (U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + (-1)x2 + x0 ≥ 0∧0 ≥ 0)

We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(25)    (x2 + (-1)x0 ≥ 0∧0 ≥ 0∧-1 + x0 + (-1)x2 ≥ 0∧x0 + (-1)x2 ≥ 0 ⇒ (U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + (-1)x0 + x2 ≥ 0∧0 ≥ 0)

We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(26)    (x14 + (-1)x0 ≥ 0∧x14 + -1 + (-1)x0 ≥ 0∧x0 + (-1)x14 ≥ 0 ⇒ (U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧0 ≥ 0∧-1 + (-1)Bound + (-1)x14 + x0 ≥ 0)

We simplified constraint (23) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(27)    (0 ≥ 0∧x9 + (-1)x0 ≥ 0∧0 ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + (-1)x0 + x9 ≥ 0)

We simplified constraint (24) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(28)    (x0 + (-1)x2 ≥ 0∧0 ≥ 0∧-1 + x2 + (-1)x0 ≥ 0∧x0 + (-1)x2 ≥ 0 ⇒ -1 + (-1)Bound + (-1)x2 + x0 ≥ 0∧0 ≥ 0∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥))

We simplified constraint (25) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(29)    (0 ≥ 0∧x2 + (-1)x0 ≥ 0∧x0 + (-1)x2 ≥ 0∧-1 + x0 + (-1)x2 ≥ 0 ⇒ (U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + (-1)x0 + x2 ≥ 0∧0 ≥ 0)

We solved constraint (26) using rule (IDP_SMT_SPLIT).We simplified constraint (27) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(30)    (0 ≥ 0∧x0 ≥ 0∧0 ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + x0 ≥ 0)

We solved constraint (28) using rule (IDP_SMT_SPLIT).We solved constraint (29) using rule (IDP_SMT_SPLIT).We simplified constraint (30) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(31)    (0 ≥ 0∧x0 ≥ 0∧0 ≥ 0∧x9 ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + x0 ≥ 0)

(32)    (0 ≥ 0∧x0 ≥ 0∧0 ≥ 0∧x9 ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + x0 ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

MINUS(x[1], y[1]) → COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1])
- ((U^Increasing(COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0)
COND(TRUE, x[3], y[3]) → MINUS(x[3], +@z(y[3], 1@z))
- (0 ≥ 0∧x0 ≥ 0∧0 ≥ 0∧x9 ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + x0 ≥ 0)
- (0 ≥ 0∧x0 ≥ 0∧0 ≥ 0∧x9 ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(MINUS(x[3], +@z(y[3], 1@z))), ≥)∧-1 + (-1)Bound + x0 ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(=@z(x₁, x₂)) = -1
POL(if(x₁, x₂, x₃)) = (-1)x₃ + (-1)x₂ + (-1)x₁
POL(TRUE) = -1
POL(MINUS(x₁, x₂)) = -1 + (-1)x₂ + x₁
POL(+@z(x₁, x₂)) = x₁ + x₂
POL(FALSE) = -1
POL(COND(x₁, x₂, x₃)) = -1 + (-1)x₃ + x₂
POL(<@z(x₁, x₂)) = -1
POL(min(x₁, x₂)) = 1 + x₂ + x₁
POL(1@z) = 1
POL(undefined) = -1

The following pairs are in P_>:

COND(TRUE, x[3], y[3]) → MINUS(x[3], +@z(y[3], 1@z))

The following pairs are in P_bound:

COND(TRUE, x[3], y[3]) → MINUS(x[3], +@z(y[3], 1@z))

The following pairs are in P_≥:

MINUS(x[1], y[1]) → COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1])

At least the following rules have been oriented under context sensitive arithmetic replacement:

+@z¹ ↔

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPNonInfProof

                ↳ IDP

                  ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

min(u, v) → if(<@z(u, v), u, v)
if(FALSE, u, v) → v
if(TRUE, u, v) → u

The integer pair graph contains the following rules and edges:

(1): MINUS(x[1], y[1]) → COND(=@z(min(x[1], y[1]), y[1]), x[1], y[1])

The set Q consists of the following terms:

cond(TRUE, x0, x1)
min(x0, x1)
if(FALSE, x0, x1)
if(TRUE, x0, x1)
minus(x0, x1)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.